es:ES, i, x:Id, T:Type, eq:EqDecider(T), v:T.
@i x initially v:T  @i only [] affect x:T  e@i. (x when e) = v 

latex

Definitions

if b then t else f fi , tt, P  Q, True, P  Q, b, , t  T, P & Q, Knd, A, A c B, @i(x:T), e@i. P(e), P  Q, EqDecider(T), x:A. B(x), False, {T}, SQType(T), @i only L affect x:T, @i x initially v:T

Lemmas

event system wf, Id wf, iff wf, bool wf, init-p wf, Knd wf, es-frame wf, es-E wf, IdLnk wf, nil member, false wf, es-kind wf, l member wf, not functionality wrt iff, Id sq, es-first-init, es-when-first-discrete, es-lc-no-change2, es-lc-le, es-le wf, es-init-le, es-lc wf, es-after wf, es-when wf, es-initially wf, es-loc-init, es-dtype wf, es-vartype wf, es-loc wf, es-isconst wf, assert wf, es-loc-lc